Nuprl Definition : refl_cl
13,42
postcript
pdf
(
E
)(
x
,
y
) == (
x
=
y
)
(
E
(
x
,
y
))
latex
clarification:
(
E
{
T
})(
x
,
y
) == (
x
=
y
T
)
(
E
(
x
,
y
))
latex
Up
gen
algebra
1
Wellformedness Lemmas
refl
cl
wf
Definitions
P
Q
origin
)(x,y) == (x = y) 
(E(x,y))
{T})(x,y) == (x = y 
T) (E(x,y)) )(x,y) == (x = y) (E(x,y))
{T})(x,y) == (x = y T) (E(x,y)) Q